poss:(ES{i}{i'}), R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}),
P:(possible-event{i:l}(poss){i'}), e:possible-event{i:l}(poss).
es-knows{i:l}(poss; R; P; e)  {i'} 

latex

Definitions	t  T, f(a), x:AB(x), , P  Q, x:A. B(x), PossibleEvent(poss), K(P)@e, Type, ES
Lemmas	event system wf, possible-event wf